Update unreducible match types error reporting #19954

EugeneFlesselle · 2024-03-15T15:23:22Z

Match type reduction can fail for any of the following reasons:

EmptyScrutinee: would be unsound to reduce
Stuck: selector does not match a case and is not provably disjoint from it either
NoInstance: selector does not uniquely determine params captures in pattern
NoMatches: selector matches none of the cases
LegacyPattern: match type contains an illegal case and sourceVersion >= 3.4

Out of those, only Stuck and NoInstance, could get reduced in a refined context.

Status quo

The match reducer returns:

ErrorType for NoMatches and LegacyPattern,
NoType, which implies the match type is left unreduced, in all other cases.

In addition, the implementation has an issue where the ErrorTypes can be left unreported, then entering the flexible type logic, thereby conforming to anything.

Proposed changes

In addition to fixing the aforementioned bug, this PR proposes to leave all unreducible match types as unreduced.
Of course the reduction may be needed at a later point for conformance, in which case the error message will still contain the same explanations from the MatchTypeTrace.

Fixes #19949
Fixes #19950

Discussion

All cases of failed match type reductions which we know will never reduce, even with refined scrutinee, should have a consistent behaviour. So NoMatches and EmptyScrutinee should either both be an error or both be left unreduced.

The current implementation attempts to do the former approach (but only for NoMatches), which has some limitations as discussed below (I'm not saying I can do better, hence the latter approach).

Undesirable errors

We dont always want an error for a NoMatches failed reduction, for example if we just need Nothing to conform to it:

trait TupleWrap[T <: Tuple]:  
  def head: Tuple.Head[T]  
  
object EmptyTupleWrap extends TupleWrap[EmptyTuple]:  
  def head = throw NoSuchElementException() // Error:
// |      ^  
// |      Match type reduction failed since selector EmptyTuple  
// |      matches none of the cases

But we could do def head: Nothing = ... to avoid the error here.

Generally speaking, places where the bounds of the match type suffice can still get a reduction error, and adding an ascription to avoid an inferred match type doesn't always do the trick.

Another refused example could be:

type Default[N <: Int] = N match  
  case 0 => 'a' | 'c'
  case 1 => 'b' | 'd'
  
def default(n: Int): Option[Default[n.type]] = n match  
  case _: (0 | 1) => Some[Default[n.type]]:  
    n match  
      case _: 0 => 'a' 
      case _: 1 => 'b'
  case _ => None  
  
default(2): Option[Char] // Error  
// |   ^  
// |   Match type reduction failed since selector (2 : Int)  
// |   matches none of the cases

even though the function looks reasonable and type-checking would be sound.

Missed errors

Also note in the EmptyTupleWrap example, we get a reduction error from a match type application which does not appear in the source code. A valid question might be when and for what exactly these conditions are checked ?

The goal is to report a type error early on for a NoMatches application right, but we are actually only doing so if we happen to do tryNormalize and end up in the MatchReducer.

Here is an example where were a match type with NoMatches is accepted

trait A:
  type X
  type R = X match
    case 0 => 'a'
    case 1 => 'b'

trait B extends A:
  type S = 2

type R1 = B#R // no error

Generally speaking, the NoMatches error can be circumvented with:

type AllowNoMatchesM[X] = {
  type X1 = X
  type R = X1 match
    case 0 => 'a'
    case 1 => 'b'
}#R
type R2 = AllowNoMatchesM[2] // no error

Also note the projections are used in the examples for simplicity but are not necessary, R can be used within B as unreduced without a reported error.

See #19799 for another example of inconsistent errors

sjrd · 2024-03-15T15:42:48Z

This would revert the semantics of match types to what they were a long time ago. I believe there were good reasons, based on practical experience, to report an error on reducing-to-nothing match types. That was however long before I started looking into match types. Perhaps @OlivierBlanvillain has some more concrete recollections?

In any case, this specific change would require a SIP at this point, unlike the other PR.

EugeneFlesselle · 2024-03-15T16:04:09Z

This would revert the semantics of match types to what they were a long time ago. I believe there were good reasons, based on practical experience, to report an error on reducing-to-nothing match types. That was however long before I started looking into match types. Perhaps @OlivierBlanvillain has some more concrete recollections?

Ah so I just found the PR #12768 which explicitly changed this.

dwijnand · 2024-03-16T14:47:03Z

Yeah, I think the users are reasonable in asking for this error eagerly.

EugeneFlesselle · 2024-03-16T17:59:39Z

For reference, I played around a bit and found the following:

With a simple case, we do get an error:

type M[X] = X match
  case 0 => 'a'
  case 1 => 'b'

type R1 = M[2] // error selector matches none of the cases

But with a setup like:

trait A:
  type X
  type R = X match
    case 0 => 'a'
    case 1 => 'b'

trait B extends A:
  type S = 2

type R2 = B#R // no error

the matches with no cases go by undetected.

Generally speaking, the rule can be circumvented with:

type AllowNoMatchesM[X] = {
  type X1 = X
  type R = X1 match
    case 0 => 'a'
    case 1 => 'b'
}#R

type R3 = AllowNoMatchesM[2] // no error

We could of course also consider this an error and try to fix it. But doing these kind of checks exhaustively seems complicated given the current implementation.

I find getting these errors in unpredictable ways worse then getting no errors at all (the second example is actually minimised from something I ran into when working with the generic tuples and was quite confused about).

EugeneFlesselle · 2024-03-16T18:24:57Z

Coming back to the original example (assuming the error is handled properly) #19949 (comment)

val t: T[Double] = new T[Double] {}
val x: t.M = "hello" // error

It also unclear to be reporting an error only on x but not t, despite its member M already being unreducible.

odersky · 2024-03-16T19:33:50Z

What is the difference between "no matches" and getting stuck?

Is "no matches" where we know that the match type cannot reduce in any refining context? In that case, I think it's reasonable to throw a type error if we know the error will be reported. I believe this can be tested with

  ctx.typeAssigner.isInstanceOf[Typer]

odersky · 2024-03-16T19:37:22Z

It's a pragmatic choice. The type system should not need any of this, but it is helpful to tell the user early that a match type makes no sense.

EugeneFlesselle · 2024-03-17T09:30:27Z

Is "no matches" where we know that the match type cannot reduce in any refining context?

Yes indeed, but it is possible for a refining context to yield a "stuck" match type, i.e. one that does not report an error.

I believe this can be tested with ctx.typeAssigner.isInstanceOf[Typer]

Ah thanks ! I found ctx.isTyper next to it which seems to be what I needed for #19953.

odersky · 2024-03-17T10:23:06Z

Yes indeed, but it is possible for a refining context to yield a "stuck" match type, i.e. one that does not report an error.

Can you point me towards a scenario where that happens?

EugeneFlesselle · 2024-03-17T10:56:43Z

Can you point me towards a scenario where that happens?

Yes, a simplistic example is:

type M[X] = X match
  case 0 => 'a'
  case 1 => 'b'

// type R1 = M[2] // error reduction failed since selector matches none of the cases

// but with a refined scrutinee:
type R2 = M[2 & 1] // no error because we do not try to reduce under an uninhabited scrutinee

In practice, this does realistically occur from outer reductions or when working with match types as members, but errors don't get reported in predictable ways: #19954 (comment)

I'm don't think keeping things as they are would be horrible either, just pointing out the current quirks with the design.

odersky · 2024-03-17T11:41:11Z

Ah, so it's because it hits the uninhabited type scrutinee! Should that also throw a TypeError then? It seems desirable that the behavior is maintained under context refinement.

EugeneFlesselle · 2024-03-17T18:59:29Z

Should that also throw a TypeError then? It seems desirable that the behavior is maintained under context refinement.

Yes I agree ! I'm trying that out now to see how much of the tests are impacted.
Reporting more errors now than previously might be harder to impose as a change than the inverse though.

Edit: Implemented in #19964

odersky · 2024-03-25T17:58:58Z

Why is bad-footprint removed? bad-footprint is an essential test. It's the only test we have that tests that match type reduction is consistent between contexts. That's the thing I have mentioned dozens of times already.

EugeneFlesselle · 2024-03-25T18:07:53Z

Why is bad-footprint removed? bad-footprint is an essential test. It's the only test we have that tests that match type reduction is consistent between contexts. That's the thing I have mentioned dozens of times already.

I should probably have added comment here in addition to the commit message.

Unfortunately, it used to only pass because of a missed ErrorType.
That said, yes we should definitely have this test, and it should definitely be re-enabled once #19434 is fixed.
I'm not sure how soon that will be though, and leaving the current ErrorTypes as is might lead to some more test cases passing for the wrong reasons being added.

EugeneFlesselle · 2024-03-25T18:11:32Z

Can we have a similar test case, but without opaque type aliases ?
It should not run into the previous issue in that case.

This reverts commit 9ae1598 Note that the changes in Typer: ``` val unsimplifiedType = result.tpe simplify(result, pt, locked) result.tpe.stripTypeVar match case e: ErrorType if !unsimplifiedType.isErroneous => errorTree(xtree, e.msg, xtree.srcPos) case _ => result ``` cannot be reverted yet since the MatchReducer now also reduces to an `ErrorType` for MatchTypeLegacyPatterns, introduced after 9ae1598.

i18488.scala was only passing because of the bug in the MatchReducer, as we can see in the subtyping trace: ``` ==> isSubType TableQuery[BaseCrudRepository.this.EntityTable] <:< Query[BaseCrudRepository.this.EntityTable, E[Option]]? ==> isSubType Query[BaseCrudRepository.this.EntityTable, Extract[BaseCrudRepository.this.EntityTable]] <:< Query[BaseCrudRepository.this.EntityTable, E[Option]] (left is approximated)? ==> isSubType E[Option] <:< Extract[BaseCrudRepository.this.EntityTable]? ==> isSubType [T[_$1]] =>> Any <:< Extract? ==> isSubType Any <:< Extract[T]? ==> isSubType Any <:< T match { case AbstractTable[t] => t } <: t (right is approximated)? ==> isSubType Any <:< <error Match type reduction failed since selector T matches none of the cases case AbstractTable[t] => t> (right is approximated)? <== isSubType Any <:< <error Match type reduction failed since selector T matches none of the cases case AbstractTable[t] => t> (right is approximated) = true <== isSubType Any <:< T match { case AbstractTable[t] => t } <: t (right is approximated) = true <== isSubType Any <:< Extract[T] = true <== isSubType [T[_$1]] =>> Any <:< Extract = true ... <== isSubType Extract[BaseCrudRepository.this.EntityTable] <:< E[Option] = true <== isSubType Query[BaseCrudRepository.this.EntityTable, Extract[BaseCrudRepository.this.EntityTable]] <:< Query[BaseCrudRepository.this.EntityTable, E[Option]] (left is approximated) = true <== isSubType TableQuery[BaseCrudRepository.this.EntityTable] <:< Query[BaseCrudRepository.this.EntityTable, E[Option]] = true ```

Modify the MatchReducer to return NoType in the case of no matches, rather than throwing a MatchTypeReductionError. This makes it consistent with the other match type reduction failures, where being stuck does not result in an error, but simply in an unreduced match type. We still get the explanations of the underlying error in the MatchTypeTrace, but in positions which need the reduction for conformance, rather than at application site of the match type.

The diff in neg/10349.scala is quite interesting. With a few intermediate values: ```scala type First[X] = X match case Map[_, v] => First[Option[v]] def first[X](x: X): First[X] = x match case x: Map[k, v] => val hdOpt: Option[v] = x.values.headOption first(hdOpt): First[Option[v]] // error only before changes ``` This now type-checks but will fail at runtime because of the in-exhaustivity of the match expression. Perhaps we should add some additional condition in `isMatchTypeShaped` to account for this, or at least emit a warning ?

`recurseWith` can be called with the same scrutinee (even if match type reduction is cached) if it is an applied match alias For example, `Tuple.Head[Tuple.Tail[T]]` will attempt to reduce `Tuple.Tail[T]` twice: - once as an argument of the match alias `Head`, and - once as a scrutinee in body of `Head` (after the substitution).

If a match type pattern is an opaque type, we use its bounds when checking the validity of the pattern. Following the ElimOpaque phase however, the pattern is beta-reduced (as normal applied type aliases), which may result in an illegal pattern.

EugeneFlesselle · 2024-03-26T13:48:08Z

The PR is now based on #20017, allowing to keep bad-footprint.scala

odersky

Nice cleanup!

EugeneFlesselle mentioned this pull request Mar 15, 2024

[WIP] Match Type with no cases should not reduce to ErrorType #19953

Closed

EugeneFlesselle mentioned this pull request Mar 16, 2024

[WIP] Handle match types reducing to ErrorType in TypeComparer #19961

Closed

EugeneFlesselle force-pushed the MatchTypeNoCases-NoType branch from 736630d to 646fea8 Compare March 16, 2024 17:42

EugeneFlesselle mentioned this pull request Mar 16, 2024

Unsound conformance from selection of member MatchType #19949

Closed

EugeneFlesselle changed the title ~~[WIP] Make match types with no matching cases not an error~~ [WIP] Leave match types with no matching cases unreduced Mar 16, 2024

EugeneFlesselle mentioned this pull request Mar 17, 2024

[WIP] Report TypeError for match type with no case or uninhabited scrutinee #19964

Closed

EugeneFlesselle force-pushed the MatchTypeNoCases-NoType branch from 646fea8 to b665f45 Compare March 20, 2024 14:16

EugeneFlesselle marked this pull request as ready for review March 20, 2024 14:32

EugeneFlesselle changed the title ~~[WIP] Leave match types with no matching cases unreduced~~ Update unreducible match types error reporting Mar 20, 2024

EugeneFlesselle requested a review from odersky March 20, 2024 14:33

EugeneFlesselle force-pushed the MatchTypeNoCases-NoType branch 2 times, most recently from 8fb447c to 3d7a77a Compare March 25, 2024 17:33

EugeneFlesselle mentioned this pull request Mar 26, 2024

Do match type reduction atPhaseNoLater than ElimOpaque #20017

Merged

EugeneFlesselle added 2 commits March 26, 2024 13:21

Add regression tests

7b69d33

EugeneFlesselle added 5 commits March 26, 2024 13:21

EugeneFlesselle force-pushed the MatchTypeNoCases-NoType branch from 3d7a77a to 2beb67e Compare March 26, 2024 12:23

odersky approved these changes Mar 27, 2024

View reviewed changes

odersky merged commit 4673f77 into scala:main Mar 27, 2024
19 checks passed

EugeneFlesselle deleted the MatchTypeNoCases-NoType branch April 6, 2024 10:51

Kordyjan added this to the 3.5.0 milestone May 10, 2024

This was referenced Jul 3, 2024

Problem with Type of Tuple.map (was: type inference regression) #15992

Closed

Backport "Update unreducible match types error reporting" to LTS #21024

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Update unreducible match types error reporting #19954

Update unreducible match types error reporting #19954

EugeneFlesselle commented Mar 15, 2024 •

edited

Loading

sjrd commented Mar 15, 2024

EugeneFlesselle commented Mar 15, 2024

dwijnand commented Mar 16, 2024

EugeneFlesselle commented Mar 16, 2024

EugeneFlesselle commented Mar 16, 2024

odersky commented Mar 16, 2024

odersky commented Mar 16, 2024

EugeneFlesselle commented Mar 17, 2024

odersky commented Mar 17, 2024

EugeneFlesselle commented Mar 17, 2024 •

edited

Loading

odersky commented Mar 17, 2024

EugeneFlesselle commented Mar 17, 2024 •

edited

Loading

odersky commented Mar 25, 2024 •

edited

Loading

EugeneFlesselle commented Mar 25, 2024 •

edited

Loading

EugeneFlesselle commented Mar 25, 2024

EugeneFlesselle commented Mar 26, 2024

odersky left a comment

Update unreducible match types error reporting #19954

Update unreducible match types error reporting #19954

Conversation

EugeneFlesselle commented Mar 15, 2024 • edited Loading

Status quo

Proposed changes

Discussion

Undesirable errors

Missed errors

sjrd commented Mar 15, 2024

EugeneFlesselle commented Mar 15, 2024

dwijnand commented Mar 16, 2024

EugeneFlesselle commented Mar 16, 2024

EugeneFlesselle commented Mar 16, 2024

odersky commented Mar 16, 2024

odersky commented Mar 16, 2024

EugeneFlesselle commented Mar 17, 2024

odersky commented Mar 17, 2024

EugeneFlesselle commented Mar 17, 2024 • edited Loading

odersky commented Mar 17, 2024

EugeneFlesselle commented Mar 17, 2024 • edited Loading

odersky commented Mar 25, 2024 • edited Loading

EugeneFlesselle commented Mar 25, 2024 • edited Loading

EugeneFlesselle commented Mar 25, 2024

EugeneFlesselle commented Mar 26, 2024

odersky left a comment

Choose a reason for hiding this comment

EugeneFlesselle commented Mar 15, 2024 •

edited

Loading

EugeneFlesselle commented Mar 17, 2024 •

edited

Loading

EugeneFlesselle commented Mar 17, 2024 •

edited

Loading

odersky commented Mar 25, 2024 •

edited

Loading

EugeneFlesselle commented Mar 25, 2024 •

edited

Loading